A,B:Type, a:EqDecider(A), b:EqDecider(B). union-deq(A; B; a; b)  EqDecider(A + B) 

latex

Definitions

s = t, strong-subtype(A; B), x:AB(x), P  Q, x:A. B(x), left + right, Type, EqDecider(T), b, axiom, t  T, prop{i:l}, sumdeq(a; b), f(a), x:A  B(x), P  Q, P  Q, P  Q, x.A(x), <a, b>, union-deq(A; B; a; b), Unit, False, , void, A, ff, , b, True, eq_bool(p; q), i <z j, i z j, (i = j), eq_atom(x; y), null(as), set_blt(p; a; b), set_le(p), x f y, set_eq(p), grp_blt(g; a; b), grp_eq(g), rng_eq(r), dcdr-to-bool(d), eq_atom{$n:n}(x; y), q_le(r; s), q_less(a; b), qeq(r; s), bimplies(p; q), band(p; q), bor(p; q), tt, , p-outcome(p), #$n, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , inl x , inr x , locl(a), Knd, (x  l), decision

Lemmas

eqtt to assert, iff transitivity, eqff to assert, assert of bnot, true wf, bool wf, bnot wf, not wf, it wf, false wf, unit wf, subtype rel wf, deq wf, sumdeq wf, iff wf, assert wf, member wf